﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Epsilon.Expr;

namespace Epsilon
{
    public abstract class PidLabel
    {
        public override bool Equals(object obj)
        {
            return (obj is PidLabel) && this == ((PidLabel)obj);
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }

        public static bool operator ==(PidLabel left, PidLabel right)
        {
            if ((left is PidBase) && (right is PidBase))
                return (PidBase)left == (PidBase)right;

            if ((left is PidTuple) && (right is PidTuple))
                return (PidTuple)left == (PidTuple)right;

            if ((left is PidFun) && (right is PidFun))
                return (PidFun)left == (PidFun)right;

            return false;
        }

        public static bool operator !=(PidLabel left, PidLabel right)
        {
            return !(left == right);
        }
    }

    public class PidBase : PidLabel
    {
        public List<PidExpr> Pids { get; private set; }
        public List<PidVar> Pidvs { get; private set; }

        public PidBase(List<PidVar> v, List<PidExpr> p)
        {
            Pids = p;
            Pidvs = v;
        }

        public bool IsEmpty
        {
            get { return Pids == null && Pidvs == null; }
        }

        public override string ToString()
        {
            if (Pids == null && Pidvs == null)
                return "{}";

            string s = "";
            if (Pidvs != null)
            {
                for (int i = 0; i < Pidvs.Count; i++)
                {
                    if (i > 0)
                        s += " + ";
                    s += Pidvs[i].ToString();
                }
            }
            if (((Pids != null) && (Pids.Count > 0)) || s == "")
            {
                if (s != "")
                    s += " + ";
                s += "{";
                for (int i = 0; i < Pids.Count; i++)
                {
                    if (i > 0)
                        s += ", ";
                    s += Pids[i].ToString();
                }
                s += "}";
            }
            return s;
        }

        public static bool operator ==(PidBase left, PidBase right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if ((left.Pids == null && right.Pids != null) ||
                (right.Pids == null && left.Pids != null))
                return false;

            if ((left.Pidvs == null && right.Pidvs != null) ||
                (right.Pidvs == null && left.Pidvs != null))
                return false;

            if (left.Pids != null)
            {
                foreach (PidExpr pe in left.Pids)
                {
                    bool found = false;
                    foreach (PidExpr ppe in right.Pids)
                    {
                        if (ppe.Pid == pe.Pid)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
                foreach (PidExpr pe in right.Pids)
                {
                    bool found = false;
                    foreach (PidExpr ppe in left.Pids)
                    {
                        if (ppe.Pid == pe.Pid)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
            }
            if (left.Pidvs != null)
            {
                foreach (PidVar pe in left.Pidvs)
                {
                    bool found = false;
                    foreach (PidVar ppe in right.Pidvs)
                    {
                        if (ppe.PidV == pe.PidV)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
                foreach (PidVar pe in right.Pidvs)
                {
                    bool found = false;
                    foreach (PidVar ppe in left.Pidvs)
                    {
                        if (ppe.PidV == pe.PidV)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
            }

            return true;
        }

        public static bool operator !=(PidBase left, PidBase right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is PidBase) && this == (PidBase)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public class PidTuple : PidLabel
    {
        public List<PidLabel> Labels { get; private set; }

        public PidTuple(List<PidLabel> ls)
        {
            Labels = ls;
        }

        public override string ToString()
        {
            string s = "{";

            for (int i = 0; i < Labels.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Labels[i].ToString();
            }

            return s + "}";
        }

        public static bool operator ==(PidTuple left, PidTuple right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Labels.Count != right.Labels.Count)
                return false;

            for (int i = 0; i < left.Labels.Count; i++)
            {
                if (left.Labels[i] != right.Labels[i])
                    return false;
            }

            return true;
        }

        public static bool operator !=(PidTuple left, PidTuple right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is PidTuple) && this == (PidTuple)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public class PidFun : PidLabel
    {
        public List<PidRLabel> Args { get; private set; }
        public PidLabel Ret { get; private set; }

        public PidFun(List<PidRLabel> a, PidLabel r)
        {
            Args = a;
            Ret = r;
        }

        public override string ToString()
        {
            string s = "fun(";

            for (int i = 0; i < Args.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Args[i].ToString();
            }

            return s + ") -> " + Ret.ToString();
        }

        // TODO alpha-conversion?
        public static bool operator ==(PidFun left, PidFun right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Args.Count != right.Args.Count)
                return false;

            bool alpha = false;
            for (int i = 0; i < left.Args.Count; i++)
            {
                if (left.Args[i] != right.Args[i])
                    alpha = true;
            }
            
            if (!alpha)
                return left.Ret == right.Ret;

            // else we alpha-convert
            try
            {
                PidRTuple temp = new PidRTuple(left.Args);

                PidRLabel newAlpha = PidUtil.CreateNewAlpha(temp);
                PidRTuple oldLeft = new PidRTuple(left.Args);
                PidRTuple oldRight = new PidRTuple(right.Args);
                Dictionary<PidVar, PidVar> subLeft = PidUtil.Equate(oldLeft, newAlpha);
                Dictionary<PidVar, PidVar> subRight = PidUtil.Equate(oldRight, newAlpha);

                return (PidUtil.AlphaConvert(left, subLeft, true).Ret ==
                    PidUtil.AlphaConvert(right, subRight, true).Ret);
            }
            catch
            {
                return false;
            }
        }

        public static bool operator !=(PidFun left, PidFun right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is PidFun) && this == (PidFun)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public abstract class PidRLabel : PidLabel
    {
        public override bool Equals(object obj)
        {
            return (obj is PidRLabel) && this == ((PidRLabel)obj);
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }

        public static bool operator ==(PidRLabel left, PidRLabel right)
        {
            if ((left is PidVar) && (right is PidVar))
                return (PidVar)left == (PidVar)right;

            if ((left is PidRTuple) && (right is PidRTuple))
                return (PidRTuple)left == (PidRTuple)right;

            if ((left is PidRFun) && (right is PidRFun))
                return (PidRFun)left == (PidRFun)right;

            return false;
        }

        public static bool operator !=(PidRLabel left, PidRLabel right)
        {
            return !(left == right);
        }
    }

    public class PidVar : PidRLabel, ISecPid
    {
        public string PidV { get; private set; }

        public PidVar(string p)
        {
            PidV = p;
        }

        public override string ToString()
        {
            return PidV;
        }

        public static bool operator ==(PidVar left, PidVar right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            return left.PidV == right.PidV;
        }

        public static bool operator !=(PidVar left, PidVar right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is PidVar) && this == (PidVar)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public class PidRTuple : PidRLabel
    {
        public List<PidRLabel> Labels { get; private set; }

        public PidRTuple(List<PidRLabel> ls)
        {
            Labels = ls;
        }

        public override string ToString()
        {
            string s = "{";

            for (int i = 0; i < Labels.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Labels[i].ToString();
            }

            return s + "}";
        }

        public static bool operator ==(PidRTuple left, PidRTuple right) 
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Labels.Count != right.Labels.Count)
                return false;

            for (int i = 0; i < left.Labels.Count; i++)
            {
                if (left.Labels[i] != right.Labels[i])
                    return false;
            }
            return true;
        }

        public static bool operator !=(PidRTuple left, PidRTuple right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is PidRTuple) && this == (PidRTuple)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public class PidRFun : PidRLabel
    {
        public List<PidRLabel> Args { get; private set; }
        public PidRLabel Ret { get; private set; }

        public PidRFun(List<PidRLabel> a, PidRLabel r)
        {
            Args = a;
            Ret = r;
        }

        public override string ToString()
        {
            string s = "fun(";

            for (int i = 0; i < Args.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Args[i].ToString();
            }

            return s + ") -> " + Ret.ToString();
        }

        // TODO alpha-conversion?
        public static bool operator ==(PidRFun left, PidRFun right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Args.Count != right.Args.Count)
                return false;

            for (int i = 0; i < left.Args.Count; i++)
            {
                if (left.Args[i] != right.Args[i])
                    return false;
            }
            return left.Ret == right.Ret;
        }

        public static bool operator !=(PidRFun left, PidRFun right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is PidRFun) && this == (PidRFun)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    [Serializable]
    public class PidLabelException : Exception
    {
        public PidLabelException() { }
        public PidLabelException(string message) : base(message) { }
        public PidLabelException(string message, Exception inner) : base(message, inner) { }
        protected PidLabelException(
          System.Runtime.Serialization.SerializationInfo info,
          System.Runtime.Serialization.StreamingContext context)
            : base(info, context) { }
    }
}
